unsolvable $M$.pre($a$,$s$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$P$ != 1of(2of(2of(2of($M$))))($a$) $\Rightarrow$ $\forall$$v$:$M$.da(locl($a$)). $\neg$$P$($s$,$v$)